times(x, plus(y, 1)) → plus(times(x, plus(y, times(1, 0))), x)
times(x, 1) → x
plus(x, 0) → x
times(x, 0) → 0
↳ QTRS
↳ DependencyPairsProof
times(x, plus(y, 1)) → plus(times(x, plus(y, times(1, 0))), x)
times(x, 1) → x
plus(x, 0) → x
times(x, 0) → 0
TIMES(x, plus(y, 1)) → PLUS(y, times(1, 0))
TIMES(x, plus(y, 1)) → PLUS(times(x, plus(y, times(1, 0))), x)
TIMES(x, plus(y, 1)) → TIMES(x, plus(y, times(1, 0)))
TIMES(x, plus(y, 1)) → TIMES(1, 0)
times(x, plus(y, 1)) → plus(times(x, plus(y, times(1, 0))), x)
times(x, 1) → x
plus(x, 0) → x
times(x, 0) → 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
TIMES(x, plus(y, 1)) → PLUS(y, times(1, 0))
TIMES(x, plus(y, 1)) → PLUS(times(x, plus(y, times(1, 0))), x)
TIMES(x, plus(y, 1)) → TIMES(x, plus(y, times(1, 0)))
TIMES(x, plus(y, 1)) → TIMES(1, 0)
times(x, plus(y, 1)) → plus(times(x, plus(y, times(1, 0))), x)
times(x, 1) → x
plus(x, 0) → x
times(x, 0) → 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
TIMES(x, plus(y, 1)) → TIMES(x, plus(y, times(1, 0)))
times(x, plus(y, 1)) → plus(times(x, plus(y, times(1, 0))), x)
times(x, 1) → x
plus(x, 0) → x
times(x, 0) → 0
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TIMES(x, plus(y, 1)) → TIMES(x, plus(y, times(1, 0)))
The value of delta used in the strict ordering is 32.
POL(plus(x1, x2)) = (3)x_1 + (4)x_2
POL(TIMES(x1, x2)) = (4)x_2
POL(times(x1, x2)) = 2
POL(1) = 4
POL(0) = 0
plus(x, 0) → x
times(x, 0) → 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
times(x, plus(y, 1)) → plus(times(x, plus(y, times(1, 0))), x)
times(x, 1) → x
plus(x, 0) → x
times(x, 0) → 0